Termination w.r.t. Q proof of /tmp/tmpsJgjak/PALINDROME_complete-noand

Termination w.r.t. Q of the following Term Rewriting System could be disproven:

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPal → tt
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPal → tt
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPal → tt
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X

Used ordering:
Polynomial interpretation [25]:

POL(U11(x₁)) = x₁
POL(U12(x₁)) = 2·x₁
POL(U13(x₁)) = 2·x₁
POL(U21(x₁)) = 2·x₁
POL(U22(x₁)) = x₁
POL(U23(x₁)) = x₁
POL(U24(x₁)) = 2·x₁
POL(U25(x₁)) = x₁
POL(U26(x₁)) = 2·x₁
POL(U31(x₁)) = 2·x₁
POL(U32(x₁)) = 2·x₁
POL(U33(x₁)) = 2·x₁
POL(U41(x₁)) = x₁
POL(U42(x₁)) = 2·x₁
POL(U43(x₁)) = x₁
POL(U44(x₁)) = x₁
POL(U45(x₁)) = x₁
POL(U46(x₁)) = x₁
POL(U51(x₁)) = 2·x₁
POL(U52(x₁)) = 2·x₁
POL(U53(x₁)) = 2·x₁
POL(U54(x₁)) = 2·x₁
POL(U55(x₁)) = 2·x₁
POL(U56(x₁)) = 2·x₁
POL(U61(x₁)) = x₁
POL(U62(x₁)) = x₁
POL(U63(x₁)) = x₁
POL(U71(x₁)) = 2·x₁
POL(U72(x₁)) = x₁
POL(U73(x₁)) = 2·x₁
POL(U74(x₁)) = 2·x₁
POL(U81(x₁)) = x₁
POL(U82(x₁)) = 2·x₁
POL(U83(x₁)) = x₁
POL(U91(x₁)) = x₁
POL(U92(x₁)) = x₁
POL(__(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 0
POL(isPal) = 0
POL(isPalListKind) = 0
POL(isQid) = 0
POL(nil) = 2
POL(tt) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPal → tt
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPal → tt
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNePal → U61(isPalListKind)
isPal → tt

Used ordering:
Polynomial interpretation [25]:

POL(U11(x₁)) = x₁
POL(U12(x₁)) = 2·x₁
POL(U13(x₁)) = 2·x₁
POL(U21(x₁)) = 2·x₁
POL(U22(x₁)) = x₁
POL(U23(x₁)) = x₁
POL(U24(x₁)) = x₁
POL(U25(x₁)) = 2·x₁
POL(U26(x₁)) = 2·x₁
POL(U31(x₁)) = 2·x₁
POL(U32(x₁)) = 2·x₁
POL(U33(x₁)) = 2·x₁
POL(U41(x₁)) = x₁
POL(U42(x₁)) = 2·x₁
POL(U43(x₁)) = 2·x₁
POL(U44(x₁)) = x₁
POL(U45(x₁)) = x₁
POL(U46(x₁)) = x₁
POL(U51(x₁)) = 2·x₁
POL(U52(x₁)) = x₁
POL(U53(x₁)) = 2·x₁
POL(U54(x₁)) = x₁
POL(U55(x₁)) = 2·x₁
POL(U56(x₁)) = x₁
POL(U61(x₁)) = x₁
POL(U62(x₁)) = 2·x₁
POL(U63(x₁)) = x₁
POL(U71(x₁)) = 1 + 2·x₁
POL(U72(x₁)) = 1 + 2·x₁
POL(U73(x₁)) = x₁
POL(U74(x₁)) = 2·x₁
POL(U81(x₁)) = 1 + x₁
POL(U82(x₁)) = 1 + 2·x₁
POL(U83(x₁)) = x₁
POL(U91(x₁)) = x₁
POL(U92(x₁)) = x₁
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 1
POL(isPal) = 1
POL(isPalListKind) = 0
POL(isQid) = 0
POL(tt) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

U61(tt) → U62(isPalListKind)
U63(tt) → tt

Used ordering:
Polynomial interpretation [25]:

POL(U11(x₁)) = 2·x₁
POL(U12(x₁)) = x₁
POL(U13(x₁)) = 2·x₁
POL(U21(x₁)) = 2·x₁
POL(U22(x₁)) = 2·x₁
POL(U23(x₁)) = x₁
POL(U24(x₁)) = 2·x₁
POL(U25(x₁)) = 2·x₁
POL(U26(x₁)) = x₁
POL(U31(x₁)) = x₁
POL(U32(x₁)) = 2·x₁
POL(U33(x₁)) = 2·x₁
POL(U41(x₁)) = 2·x₁
POL(U42(x₁)) = x₁
POL(U43(x₁)) = x₁
POL(U44(x₁)) = 2·x₁
POL(U45(x₁)) = x₁
POL(U46(x₁)) = 2·x₁
POL(U51(x₁)) = 2·x₁
POL(U52(x₁)) = 2·x₁
POL(U53(x₁)) = x₁
POL(U54(x₁)) = 2·x₁
POL(U55(x₁)) = x₁
POL(U56(x₁)) = x₁
POL(U61(x₁)) = 2 + 2·x₁
POL(U62(x₁)) = 1 + 2·x₁
POL(U63(x₁)) = 1 + x₁
POL(U71(x₁)) = 2·x₁
POL(U72(x₁)) = 2·x₁
POL(U73(x₁)) = 2·x₁
POL(U74(x₁)) = 2·x₁
POL(U81(x₁)) = x₁
POL(U82(x₁)) = x₁
POL(U83(x₁)) = x₁
POL(U91(x₁)) = x₁
POL(U92(x₁)) = x₁
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 0
POL(isPal) = 0
POL(isPalListKind) = 0
POL(isQid) = 0
POL(tt) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U62(tt) → U63(isQid)
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U62(tt) → U63(isQid)
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

U62(tt) → U63(isQid)

Used ordering:
Polynomial interpretation [25]:

POL(U11(x₁)) = x₁
POL(U12(x₁)) = 2·x₁
POL(U13(x₁)) = 2·x₁
POL(U21(x₁)) = 2·x₁
POL(U22(x₁)) = x₁
POL(U23(x₁)) = x₁
POL(U24(x₁)) = 2·x₁
POL(U25(x₁)) = 2·x₁
POL(U26(x₁)) = 2·x₁
POL(U31(x₁)) = 2·x₁
POL(U32(x₁)) = x₁
POL(U33(x₁)) = 2·x₁
POL(U41(x₁)) = 2·x₁
POL(U42(x₁)) = x₁
POL(U43(x₁)) = x₁
POL(U44(x₁)) = 2·x₁
POL(U45(x₁)) = 2·x₁
POL(U46(x₁)) = 2·x₁
POL(U51(x₁)) = x₁
POL(U52(x₁)) = 2·x₁
POL(U53(x₁)) = 2·x₁
POL(U54(x₁)) = 2·x₁
POL(U55(x₁)) = 2·x₁
POL(U56(x₁)) = x₁
POL(U62(x₁)) = 2 + 2·x₁
POL(U63(x₁)) = 1 + x₁
POL(U71(x₁)) = 2·x₁
POL(U72(x₁)) = x₁
POL(U73(x₁)) = 2·x₁
POL(U74(x₁)) = 2·x₁
POL(U81(x₁)) = 2·x₁
POL(U82(x₁)) = 2·x₁
POL(U83(x₁)) = x₁
POL(U91(x₁)) = x₁
POL(U92(x₁)) = 2·x₁
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 0
POL(isPal) = 0
POL(isPalListKind) = 0
POL(isQid) = 0
POL(tt) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

U51¹(tt) → ISPALLISTKIND
U55¹(tt) → ISLIST
U52¹(tt) → ISPALLISTKIND
U22¹(tt) → ISPALLISTKIND
U31¹(tt) → U32¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
ISLIST → ISPALLISTKIND
U44¹(tt) → U45¹(isList)
U43¹(tt) → U44¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)
U31¹(tt) → ISPALLISTKIND
U22¹(tt) → U23¹(isPalListKind)
U42¹(tt) → ISPALLISTKIND
U54¹(tt) → ISNELIST
ISPAL → ISPALLISTKIND
U11¹(tt) → U12¹(isPalListKind)
U44¹(tt) → ISLIST
ISNEPAL → U71¹(isQid)
U25¹(tt) → ISLIST
U73¹(tt) → U74¹(isPalListKind)
U23¹(tt) → ISPALLISTKIND
ISNELIST → ISPALLISTKIND
U73¹(tt) → ISPALLISTKIND
U55¹(tt) → U56¹(isList)
U45¹(tt) → ISNELIST
U54¹(tt) → U55¹(isNeList)
U24¹(tt) → ISLIST
U82¹(tt) → ISNEPAL
U72¹(tt) → U73¹(isPal)
U24¹(tt) → U25¹(isList)
U53¹(tt) → ISPALLISTKIND
U82¹(tt) → U83¹(isNePal)
U45¹(tt) → U46¹(isNeList)
U32¹(tt) → U33¹(isQid)
U81¹(tt) → ISPALLISTKIND
U41¹(tt) → U42¹(isPalListKind)
ISPAL → U81¹(isPalListKind)
U71¹(tt) → U72¹(isPalListKind)
U12¹(tt) → U13¹(isNeList)
ISLIST → U11¹(isPalListKind)
U72¹(tt) → ISPAL
U11¹(tt) → ISPALLISTKIND
U21¹(tt) → U22¹(isPalListKind)
U91¹(tt) → ISPALLISTKIND
U71¹(tt) → ISPALLISTKIND
ISNEPAL → ISQID
U41¹(tt) → ISPALLISTKIND
U81¹(tt) → U82¹(isPalListKind)
ISPALLISTKIND → ISPALLISTKIND
U23¹(tt) → U24¹(isPalListKind)
ISNELIST → U51¹(isPalListKind)
ISNELIST → U31¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U32¹(tt) → ISQID
U25¹(tt) → U26¹(isList)
U12¹(tt) → ISNELIST
ISPALLISTKIND → U91¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U91¹(tt) → U92¹(isPalListKind)
ISNELIST → U41¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → ISPALLISTKIND
U43¹(tt) → ISPALLISTKIND

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U51¹(tt) → ISPALLISTKIND
U55¹(tt) → ISLIST
U52¹(tt) → ISPALLISTKIND
U22¹(tt) → ISPALLISTKIND
U31¹(tt) → U32¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
ISLIST → ISPALLISTKIND
U44¹(tt) → U45¹(isList)
U43¹(tt) → U44¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)
U31¹(tt) → ISPALLISTKIND
U22¹(tt) → U23¹(isPalListKind)
U42¹(tt) → ISPALLISTKIND
U54¹(tt) → ISNELIST
ISPAL → ISPALLISTKIND
U11¹(tt) → U12¹(isPalListKind)
U44¹(tt) → ISLIST
ISNEPAL → U71¹(isQid)
U25¹(tt) → ISLIST
U73¹(tt) → U74¹(isPalListKind)
U23¹(tt) → ISPALLISTKIND
ISNELIST → ISPALLISTKIND
U73¹(tt) → ISPALLISTKIND
U55¹(tt) → U56¹(isList)
U45¹(tt) → ISNELIST
U54¹(tt) → U55¹(isNeList)
U24¹(tt) → ISLIST
U82¹(tt) → ISNEPAL
U72¹(tt) → U73¹(isPal)
U24¹(tt) → U25¹(isList)
U53¹(tt) → ISPALLISTKIND
U82¹(tt) → U83¹(isNePal)
U45¹(tt) → U46¹(isNeList)
U32¹(tt) → U33¹(isQid)
U81¹(tt) → ISPALLISTKIND
U41¹(tt) → U42¹(isPalListKind)
ISPAL → U81¹(isPalListKind)
U71¹(tt) → U72¹(isPalListKind)
U12¹(tt) → U13¹(isNeList)
ISLIST → U11¹(isPalListKind)
U72¹(tt) → ISPAL
U11¹(tt) → ISPALLISTKIND
U21¹(tt) → U22¹(isPalListKind)
U91¹(tt) → ISPALLISTKIND
U71¹(tt) → ISPALLISTKIND
ISNEPAL → ISQID
U41¹(tt) → ISPALLISTKIND
U81¹(tt) → U82¹(isPalListKind)
ISPALLISTKIND → ISPALLISTKIND
U23¹(tt) → U24¹(isPalListKind)
ISNELIST → U51¹(isPalListKind)
ISNELIST → U31¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U32¹(tt) → ISQID
U25¹(tt) → U26¹(isList)
U12¹(tt) → ISNELIST
ISPALLISTKIND → U91¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U91¹(tt) → U92¹(isPalListKind)
ISNELIST → U41¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → ISPALLISTKIND
U43¹(tt) → ISPALLISTKIND

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 30 less nodes.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                            ↳ UsableRulesProof

                          ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPALLISTKIND → U91¹(isPalListKind)
ISPALLISTKIND → ISPALLISTKIND
U91¹(tt) → ISPALLISTKIND

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                          ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPALLISTKIND → U91¹(isPalListKind)
ISPALLISTKIND → ISPALLISTKIND
U91¹(tt) → ISPALLISTKIND

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISPALLISTKIND → U91¹(isPalListKind) at position [0] we obtained the following new rules:

ISPALLISTKIND → U91¹(tt)
ISPALLISTKIND → U91¹(U91(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ NonTerminationProof

                          ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPALLISTKIND → U91¹(U91(isPalListKind))
ISPALLISTKIND → U91¹(tt)
ISPALLISTKIND → ISPALLISTKIND
U91¹(tt) → ISPALLISTKIND

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

ISPALLISTKIND → U91¹(U91(isPalListKind))
ISPALLISTKIND → U91¹(tt)
ISPALLISTKIND → ISPALLISTKIND
U91¹(tt) → ISPALLISTKIND

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

s = ISPALLISTKIND evaluates to t =ISPALLISTKIND

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ISPALLISTKIND to ISPALLISTKIND.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U82¹(tt) → ISNEPAL
U71¹(tt) → U72¹(isPalListKind)
U81¹(tt) → U82¹(isPalListKind)
U72¹(tt) → ISPAL
ISNEPAL → U71¹(isQid)
ISPAL → U81¹(isPalListKind)

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U82¹(tt) → ISNEPAL
U71¹(tt) → U72¹(isPalListKind)
U81¹(tt) → U82¹(isPalListKind)
U72¹(tt) → ISPAL
ISPAL → U81¹(isPalListKind)
ISNEPAL → U71¹(isQid)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNEPAL → U71¹(isQid) at position [0] we obtained the following new rules:

ISNEPAL → U71¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ UsableRulesProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U82¹(tt) → ISNEPAL
U71¹(tt) → U72¹(isPalListKind)
U81¹(tt) → U82¹(isPalListKind)
ISNEPAL → U71¹(tt)
U72¹(tt) → ISPAL
ISPAL → U81¹(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isQid → tt

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ Narrowing

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U82¹(tt) → ISNEPAL
U71¹(tt) → U72¹(isPalListKind)
U81¹(tt) → U82¹(isPalListKind)
U72¹(tt) → ISPAL
ISNEPAL → U71¹(tt)
ISPAL → U81¹(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U71¹(tt) → U72¹(isPalListKind) at position [0] we obtained the following new rules:

U71¹(tt) → U72¹(U91(isPalListKind))
U71¹(tt) → U72¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U82¹(tt) → ISNEPAL
U71¹(tt) → U72¹(tt)
U81¹(tt) → U82¹(isPalListKind)
ISNEPAL → U71¹(tt)
U72¹(tt) → ISPAL
U71¹(tt) → U72¹(U91(isPalListKind))
ISPAL → U81¹(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U81¹(tt) → U82¹(isPalListKind) at position [0] we obtained the following new rules:

U81¹(tt) → U82¹(tt)
U81¹(tt) → U82¹(U91(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U82¹(tt) → ISNEPAL
U81¹(tt) → U82¹(tt)
U81¹(tt) → U82¹(U91(isPalListKind))
U71¹(tt) → U72¹(tt)
U72¹(tt) → ISPAL
ISNEPAL → U71¹(tt)
U71¹(tt) → U72¹(U91(isPalListKind))
ISPAL → U81¹(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISPAL → U81¹(isPalListKind) at position [0] we obtained the following new rules:

ISPAL → U81¹(tt)
ISPAL → U81¹(U91(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ NonTerminationProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U82¹(tt) → ISNEPAL
U81¹(tt) → U82¹(tt)
ISPAL → U81¹(U91(isPalListKind))
U71¹(tt) → U72¹(tt)
U81¹(tt) → U82¹(U91(isPalListKind))
ISNEPAL → U71¹(tt)
U72¹(tt) → ISPAL
ISPAL → U81¹(tt)
U71¹(tt) → U72¹(U91(isPalListKind))

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

U82¹(tt) → ISNEPAL
U81¹(tt) → U82¹(tt)
ISPAL → U81¹(U91(isPalListKind))
U71¹(tt) → U72¹(tt)
U81¹(tt) → U82¹(U91(isPalListKind))
ISNEPAL → U71¹(tt)
U72¹(tt) → ISPAL
ISPAL → U81¹(tt)
U71¹(tt) → U72¹(U91(isPalListKind))

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

s = ISNEPAL evaluates to t =ISNEPAL

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

ISNEPAL → U71¹(tt)
with rule ISNEPAL → U71¹(tt) at position [] and matcher [ ]

U71¹(tt) → U72¹(tt)
with rule U71¹(tt) → U72¹(tt) at position [] and matcher [ ]

U72¹(tt) → ISPAL
with rule U72¹(tt) → ISPAL at position [] and matcher [ ]

ISPAL → U81¹(tt)
with rule ISPAL → U81¹(tt) at position [] and matcher [ ]

U81¹(tt) → U82¹(tt)
with rule U81¹(tt) → U82¹(tt) at position [] and matcher [ ]

U82¹(tt) → ISNEPAL
with rule U82¹(tt) → ISNEPAL

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

U22¹(tt) → U23¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U54¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U23¹(tt) → U24¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
U44¹(tt) → ISLIST
U41¹(tt) → U42¹(isPalListKind)
ISNELIST → U51¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U25¹(tt) → ISLIST
U51¹(tt) → U52¹(isPalListKind)
U12¹(tt) → ISNELIST
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
ISLIST → U11¹(isPalListKind)
ISNELIST → U41¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U24¹(tt) → ISLIST
U21¹(tt) → U22¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U22¹(tt) → U23¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U54¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U23¹(tt) → U24¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
U44¹(tt) → ISLIST
U41¹(tt) → U42¹(isPalListKind)
ISNELIST → U51¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U25¹(tt) → ISLIST
U51¹(tt) → U52¹(isPalListKind)
U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(isList)
U52¹(tt) → U53¹(isPalListKind)
ISLIST → U11¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
ISNELIST → U41¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U22¹(tt) → U23¹(isPalListKind) at position [0] we obtained the following new rules:

U22¹(tt) → U23¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U24¹(tt) → U25¹(isList)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U41¹(tt) → U42¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U44¹(tt) → U45¹(isList)
ISLIST → U11¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)
U22¹(tt) → U23¹(U91(isPalListKind))
U54¹(tt) → ISNELIST
U23¹(tt) → U24¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISNELIST → U51¹(isPalListKind)
U44¹(tt) → ISLIST
U53¹(tt) → U54¹(isPalListKind)
U25¹(tt) → ISLIST
U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
ISNELIST → U41¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U24¹(tt) → U25¹(isList) at position [0] we obtained the following new rules:

U24¹(tt) → U25¹(tt)
U24¹(tt) → U25¹(U21(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U41¹(tt) → U42¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U44¹(tt) → U45¹(isList)
ISLIST → U11¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U24¹(tt) → U25¹(U21(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
U23¹(tt) → U24¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
U44¹(tt) → ISLIST
ISNELIST → U51¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U25¹(tt) → ISLIST
U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
U24¹(tt) → U25¹(tt)
U54¹(tt) → U55¹(isNeList)
ISNELIST → U41¹(isPalListKind)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U23¹(tt) → U24¹(isPalListKind) at position [0] we obtained the following new rules:

U23¹(tt) → U24¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U41¹(tt) → U42¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U44¹(tt) → U45¹(isList)
ISLIST → U11¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U24¹(tt) → U25¹(U21(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
U11¹(tt) → U12¹(isPalListKind)
U23¹(tt) → U24¹(tt)
ISNELIST → U51¹(isPalListKind)
U44¹(tt) → ISLIST
U53¹(tt) → U54¹(isPalListKind)
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
ISNELIST → U41¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U24¹(tt) → U25¹(tt)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U11¹(tt) → U12¹(isPalListKind) at position [0] we obtained the following new rules:

U11¹(tt) → U12¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U41¹(tt) → U42¹(isPalListKind)
U11¹(tt) → U12¹(U91(isPalListKind))
U51¹(tt) → U52¹(isPalListKind)
U44¹(tt) → U45¹(isList)
ISLIST → U11¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U24¹(tt) → U25¹(U21(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U51¹(isPalListKind)
U23¹(tt) → U24¹(tt)
U53¹(tt) → U54¹(isPalListKind)
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
U24¹(tt) → U25¹(tt)
U54¹(tt) → U55¹(isNeList)
ISNELIST → U41¹(isPalListKind)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U41¹(tt) → U42¹(isPalListKind) at position [0] we obtained the following new rules:

U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U51¹(tt) → U52¹(isPalListKind)
U11¹(tt) → U12¹(U91(isPalListKind))
U44¹(tt) → U45¹(isList)
ISLIST → U11¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U41¹(tt) → U42¹(U91(isPalListKind))
U24¹(tt) → U25¹(U21(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
U23¹(tt) → U24¹(tt)
ISNELIST → U51¹(isPalListKind)
U44¹(tt) → ISLIST
U53¹(tt) → U54¹(isPalListKind)
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
ISNELIST → U41¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U24¹(tt) → U25¹(tt)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNELIST → U51¹(isPalListKind) at position [0] we obtained the following new rules:

ISNELIST → U51¹(U91(isPalListKind))
ISNELIST → U51¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U11¹(tt) → U12¹(U91(isPalListKind))
U51¹(tt) → U52¹(isPalListKind)
ISNELIST → U51¹(tt)
U44¹(tt) → U45¹(isList)
ISLIST → U11¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U24¹(tt) → U25¹(U21(isPalListKind))
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
U23¹(tt) → U24¹(tt)
U53¹(tt) → U54¹(isPalListKind)
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
U24¹(tt) → U25¹(tt)
U54¹(tt) → U55¹(isNeList)
ISNELIST → U41¹(isPalListKind)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U53¹(tt) → U54¹(isPalListKind) at position [0] we obtained the following new rules:

U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U51¹(tt) → U52¹(isPalListKind)
U11¹(tt) → U12¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U44¹(tt) → U45¹(isList)
ISLIST → U11¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U41¹(tt) → U42¹(U91(isPalListKind))
U24¹(tt) → U25¹(U21(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
U23¹(tt) → U24¹(tt)
U44¹(tt) → ISLIST
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
ISNELIST → U41¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U24¹(tt) → U25¹(tt)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U51¹(tt) → U52¹(isPalListKind) at position [0] we obtained the following new rules:

U51¹(tt) → U52¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U11¹(tt) → U12¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U51¹(tt) → U52¹(tt)
U44¹(tt) → U45¹(isList)
ISLIST → U11¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U24¹(tt) → U25¹(U21(isPalListKind))
U41¹(tt) → U42¹(U91(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
U23¹(tt) → U24¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
U24¹(tt) → U25¹(tt)
U54¹(tt) → U55¹(isNeList)
ISNELIST → U41¹(isPalListKind)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U44¹(tt) → U45¹(isList) at position [0] we obtained the following new rules:

U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U44¹(tt) → U45¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U44¹(tt) → U45¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U51¹(tt) → U52¹(tt)
ISLIST → U11¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U41¹(tt) → U42¹(U91(isPalListKind))
U24¹(tt) → U25¹(U21(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
U23¹(tt) → U24¹(tt)
U44¹(tt) → ISLIST
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
U44¹(tt) → U45¹(U11(isPalListKind))
ISNELIST → U41¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U24¹(tt) → U25¹(tt)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U52¹(tt) → U53¹(isPalListKind) at position [0] we obtained the following new rules:

U52¹(tt) → U53¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ Narrowing

                                                                      ↳ QDP

                                                                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U52¹(tt) → U53¹(tt)
U44¹(tt) → U45¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
U52¹(tt) → U53¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U51¹(tt) → U52¹(tt)
ISLIST → U11¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U24¹(tt) → U25¹(U21(isPalListKind))
U41¹(tt) → U42¹(U91(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
U23¹(tt) → U24¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U54¹(tt) → U55¹(isNeList)
ISNELIST → U41¹(isPalListKind)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISLIST → U11¹(isPalListKind) at position [0] we obtained the following new rules:

ISLIST → U11¹(U91(isPalListKind))
ISLIST → U11¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ Narrowing

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U44¹(tt) → U45¹(tt)
U52¹(tt) → U53¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
U52¹(tt) → U53¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U51¹(tt) → U52¹(tt)
ISLIST → U11¹(tt)
U21¹(tt) → U22¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U41¹(tt) → U42¹(U91(isPalListKind))
U24¹(tt) → U25¹(U21(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
ISLIST → U11¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)
U44¹(tt) → ISLIST
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(U11(isPalListKind))
ISNELIST → U41¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U24¹(tt) → U25¹(tt)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNELIST → U41¹(isPalListKind) at position [0] we obtained the following new rules:

ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ Narrowing

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U52¹(tt) → U53¹(tt)
U44¹(tt) → U45¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
U52¹(tt) → U53¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U51¹(tt) → U52¹(tt)
U43¹(tt) → U44¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
ISLIST → U11¹(tt)
U24¹(tt) → U25¹(U21(isPalListKind))
U41¹(tt) → U42¹(U91(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
ISLIST → U11¹(U91(isPalListKind))
U44¹(tt) → ISLIST
U23¹(tt) → U24¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
ISNELIST → U41¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U54¹(tt) → U55¹(isNeList)
ISNELIST → U41¹(tt)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U54¹(tt) → U55¹(isNeList) at position [0] we obtained the following new rules:

U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ Narrowing

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U54¹(tt) → U55¹(U41(isPalListKind))
U44¹(tt) → U45¹(tt)
U52¹(tt) → U53¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
U52¹(tt) → U53¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U51¹(tt) → U52¹(tt)
ISLIST → U11¹(tt)
U21¹(tt) → U22¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U41¹(tt) → U42¹(U91(isPalListKind))
U24¹(tt) → U25¹(U21(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
ISLIST → U11¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)
U44¹(tt) → ISLIST
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U54¹(tt) → U55¹(U31(isPalListKind))
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
ISNELIST → U41¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U24¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISLIST → U21¹(isPalListKind)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U21¹(tt) → U22¹(isPalListKind) at position [0] we obtained the following new rules:

U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ Narrowing

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ Narrowing

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U54¹(tt) → U55¹(U41(isPalListKind))
U52¹(tt) → U53¹(tt)
U44¹(tt) → U45¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
U52¹(tt) → U53¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U51¹(tt) → U52¹(tt)
U43¹(tt) → U44¹(isPalListKind)
ISLIST → U11¹(tt)
U24¹(tt) → U25¹(U21(isPalListKind))
U41¹(tt) → U42¹(U91(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
U54¹(tt) → U55¹(U51(isPalListKind))
U21¹(tt) → U22¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
ISLIST → U11¹(U91(isPalListKind))
U44¹(tt) → ISLIST
U23¹(tt) → U24¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U54¹(tt) → U55¹(U31(isPalListKind))
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
ISNELIST → U41¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
ISNELIST → U41¹(tt)
U24¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U43¹(tt) → U44¹(isPalListKind) at position [0] we obtained the following new rules:

U43¹(tt) → U44¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ Narrowing

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ Narrowing

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U54¹(tt) → U55¹(U41(isPalListKind))
U44¹(tt) → U45¹(tt)
U52¹(tt) → U53¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
U52¹(tt) → U53¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U43¹(tt) → U44¹(tt)
U51¹(tt) → U52¹(tt)
ISLIST → U11¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U24¹(tt) → U25¹(U21(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
ISNELIST → U51¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
ISLIST → U11¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)
U44¹(tt) → ISLIST
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U54¹(tt) → U55¹(U31(isPalListKind))
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
ISNELIST → U41¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U24¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISLIST → U21¹(isPalListKind) at position [0] we obtained the following new rules:

ISLIST → U21¹(U91(isPalListKind))
ISLIST → U21¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ Narrowing

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ Narrowing

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ Narrowing

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U43¹(tt) → U44¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U54¹(tt) → U55¹(U41(isPalListKind))
U52¹(tt) → U53¹(tt)
U44¹(tt) → U45¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
U52¹(tt) → U53¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U51¹(tt) → U52¹(tt)
U43¹(tt) → U44¹(tt)
ISLIST → U11¹(tt)
U24¹(tt) → U25¹(U21(isPalListKind))
U41¹(tt) → U42¹(U91(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U42¹(tt) → U43¹(isPalListKind)
U54¹(tt) → U55¹(U51(isPalListKind))
U21¹(tt) → U22¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
ISLIST → U11¹(U91(isPalListKind))
U44¹(tt) → ISLIST
U23¹(tt) → U24¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U54¹(tt) → U55¹(U31(isPalListKind))
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
ISNELIST → U41¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
ISNELIST → U41¹(tt)
U24¹(tt) → ISLIST
U21¹(tt) → U22¹(U91(isPalListKind))
ISLIST → U21¹(tt)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U42¹(tt) → U43¹(isPalListKind) at position [0] we obtained the following new rules:

U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ Narrowing

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ Narrowing

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ Narrowing

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

U42¹(tt) → U43¹(tt)
U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U43¹(tt) → U44¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U54¹(tt) → U55¹(U41(isPalListKind))
U42¹(tt) → U43¹(U91(isPalListKind))
U44¹(tt) → U45¹(tt)
U52¹(tt) → U53¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
U52¹(tt) → U53¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U43¹(tt) → U44¹(tt)
U51¹(tt) → U52¹(tt)
ISLIST → U11¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U24¹(tt) → U25¹(U21(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISNELIST → U51¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
ISLIST → U11¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)
U44¹(tt) → ISLIST
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U54¹(tt) → U55¹(U31(isPalListKind))
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
ISNELIST → U41¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U24¹(tt) → ISLIST
ISNELIST → U41¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))
ISLIST → U21¹(tt)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

U42¹(tt) → U43¹(tt)
U53¹(tt) → U54¹(tt)
U41¹(tt) → U42¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U43¹(tt) → U44¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U55¹(tt) → ISLIST
U54¹(tt) → U55¹(U41(isPalListKind))
U42¹(tt) → U43¹(U91(isPalListKind))
U44¹(tt) → U45¹(tt)
U52¹(tt) → U53¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
U52¹(tt) → U53¹(U91(isPalListKind))
ISNELIST → U51¹(tt)
U43¹(tt) → U44¹(tt)
U51¹(tt) → U52¹(tt)
ISLIST → U11¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U24¹(tt) → U25¹(U21(isPalListKind))
U44¹(tt) → U45¹(U21(isPalListKind))
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISNELIST → U51¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U54¹(tt) → ISNELIST
ISLIST → U11¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)
U44¹(tt) → ISLIST
U51¹(tt) → U52¹(U91(isPalListKind))
U25¹(tt) → ISLIST
U54¹(tt) → U55¹(U31(isPalListKind))
U23¹(tt) → U24¹(U91(isPalListKind))
U12¹(tt) → ISNELIST
ISNELIST → U41¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U45¹(tt) → ISNELIST
U44¹(tt) → U45¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U24¹(tt) → ISLIST
ISNELIST → U41¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))
ISLIST → U21¹(tt)

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

s = U54¹(tt) evaluates to t =U54¹(tt)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U54¹(tt) → ISNELIST
with rule U54¹(tt) → ISNELIST at position [] and matcher [ ]

ISNELIST → U51¹(tt)
with rule ISNELIST → U51¹(tt) at position [] and matcher [ ]

U51¹(tt) → U52¹(tt)
with rule U51¹(tt) → U52¹(tt) at position [] and matcher [ ]

U52¹(tt) → U53¹(tt)
with rule U52¹(tt) → U53¹(tt) at position [] and matcher [ ]

U53¹(tt) → U54¹(tt)
with rule U53¹(tt) → U54¹(tt)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.